A, B, C:Dsys.
A || B  interface-compatible(C;A)  interface-compatible(C;B)  interface-compatible(C;A  B) 

latex

Definitions

x:A. B(x), Dsys, P  Q, t  T, interface-compatible(A;B), A  B, P & Q, interface-link(A;B;l;tg), M.dout(l,tg), M.din(l,tg), rcv(l,tg) declared in M, A, M1  M2, b, 1of(t), 2of(t), f(x)?z, Top, Prop, mk-ma, if b t else f fi, x. t(x), true, True, P  Q, false, SQType(T), {T}, MsgA, Valtype(da;k), x(s), , Unit, P  Q, P  Q, False,

Lemmas

interface-compatible wf, m-sys-compatible wf, Id wf, msga wf, lsrc wf, ldst wf, rcv wf, Knd wf, fpf-join-cap-sq, Kind-deq wf, fpf-trivial-subtype-top, fpf-dom wf, bool wf, eqtt to assert, fpf-join-dom2, bool cases, bool sq, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-join wf, top wf, fpf-cap wf, btrue wf, fpf-ap wf, bfalse wf, interface-link wf, ifthenelse wf, IdLnk wf